(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/relations.ma".

inductive atom_ : Type[0] ≝ 
| a : atom_
| l : atom_ → atom_. 

notation "𝐒" with precedence 45 for @{structure}.

inductive structure : Type[0] ≝
| par :  𝐒 →  𝐒  →  𝐒 
| neg :  𝐒  →  𝐒 
| seq :  𝐒  →  𝐒  →  𝐒 
| copar:  𝐒 →  𝐒  →  𝐒 
| atom : atom_→  𝐒 
| unit :  𝐒 .

notation "❲x❳" with precedence 45
for @{atom $x}.

notation "𝐚" with precedence 45 for @{❲a❳}.
notation "𝐛" with precedence 45 for @{❲l a❳}.
notation "𝐜" with precedence 45 for @{❲l (l a)❳}.
notation "𝐝" with precedence 45 for @{❲l (l (l a))❳}.

notation "[x,y]" with precedence 45
for @{par $x $y}.

notation "〈x;y〉" with precedence 45
for @{seq $x $y}.

notation "❨x,y❩" with precedence 45
for @{copar $x $y}.

notation "○" with precedence 45
for @{unit}.

notation "x ≡ y" with precedence 45 (* ≈ non me lo lascia usare *)
for @{modulo $x $y}.

inductive modulo :  𝐒  →  𝐒  → Prop ≝
 | modComm : ∀S1,S2: 𝐒 .              S1 ≡ S2 → S2 ≡ S1
 | modRif : ∀S1: 𝐒 .                  S1 ≡ S1
 | modTrans : ∀S1,S2,S3: 𝐒 .          S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3
 
 | modParContext : ∀S1,S2,S3: 𝐒 .     S1 ≡ S3 → ([S1,S2]) ≡ ([S3,S2]) 
 | modNegContext : ∀S1,S2: 𝐒 .        S1 ≡ S2 → (neg S1) ≡ (neg S2)
 | modCoparContext: ∀S1,S2,S3: 𝐒 .    S1 ≡ S3 → (❨S1,S2❩) ≡ (❨S3,S2❩)
 | modSeqContext1: ∀S1,S2,S3: 𝐒 .     S1 ≡ S3 → (〈S1;S2〉) ≡ (〈S3;S2〉)
 | modSeqContext2: ∀S1,S2,S3: 𝐒 .     S1 ≡ S3 → (〈S2;S1〉) ≡ (〈S2;S3〉)
  
 | modParAss : ∀S1,S2,S3: 𝐒 .         ([S1,[S2,S3]]) ≡ ([[S1,S2],S3])
 | modParCom : ∀S1,S2: 𝐒 .            ([S1,S2]) ≡ ([S2,S1])
 | modParUnit: ∀S: 𝐒 .                ([○,S]) ≡ S
 
 | modCoparAss: ∀S1,S2,S3: 𝐒 .        (❨S1,❨S2,S3❩❩) ≡ (❨❨S1,S2❩,S3❩)
 | modCoparCom: ∀S1,S2: 𝐒 .           (❨S1,S2❩) ≡ (❨S2,S1❩)
 | modCoparUnit: ∀S: 𝐒 .              (❨○,S❩) ≡ S 
 
 | modSeqAss : ∀S1,S2,S3: 𝐒 .         (〈S1;〈S2;S3〉〉) ≡ (〈〈S1;S2〉;S3〉) (* ???? *)
 | modSeqUnit1 : ∀S: 𝐒 .              (〈○;S〉) ≡ S 
 | modSeqUnit2 : ∀S: 𝐒 .              (〈S;○〉) ≡ S 
 
 | modNegUnit:                              (neg (○)) ≡ (○)
 | modNegIdem: ∀S: 𝐒 .                (neg (neg S)) ≡ (S) 
 
 | modNegPar: ∀S1,S2: 𝐒 .             (neg ([S1,S2])) ≡ (❨(neg S1),(neg S2)❩)
 | modNegCopar: ∀S1,S2: 𝐒 .           (neg (❨S1,S2❩)) ≡ ([neg S1, neg S2])
 | modNegSeq: ∀S1,S2: 𝐒 .             (neg (〈S1;S2〉)) ≡ (〈neg S1; neg S2〉)
.







lemma prova1 : ∀S: 𝐒 . S ≡ [S,○].

#H3 

@(modTrans ? ([○,H3]) ?)  [1: @modComm @modParUnit |  @(modParCom ? ?) qed.

 
lemma prova13: ∀S1,S2,S3: 𝐒 . S1 ≡S3 → [S2,S1] ≡ [S2,S3].

#H16 #H17 #H18 #H19 @(modTrans ([H17,H16]) ([H16,H17]) ([H17,H18])) [ @modParCom ] 
@modComm @(modTrans ? ([H18,H17]) ?) [ @modParCom ] @(modParContext ? ? ?) @modComm @H19 qed. 


lemma prova14: ∀S1,S2,S3,S4:  𝐒 . S1≡S2 → S3 ≡ S4 → [S1,S3] ≡ [S2,S4]. 
#H68 #H69 #H70 #H71 #H72 #H73 @(modTrans ([H68,H70]) ([H69,H70]) ([H69,H71])) 
[ @(modParContext ? H70 ?) @H72 ] @prova13 @H73 qed.


lemma prova2 : ∀S1,S2,S3: 𝐒 . [S1,[S2,S3]] ≡ [[S3,S2],S1].

#H3 #H4 #H5 @(modTrans ? ([[H3,H4],H5]) ?) [ @modParAss ]
@modComm @(modTrans ? ([H5,[H4,H3]]) ?) [ @(modTrans ? ([H3,[H5,H4]]) ?) [ // ] 
@modComm @(modTrans ? ([[H5,H4],H3]) ?)  [ @modParAss | @modParCom ] |
@modComm @(modTrans ? ([H5,[H3,H4]]) ?) [ @modParCom | @prova13 @modParCom qed.


lemma prova3:[〈[○,○];❨○,○❩〉,○] ≡ ○.

@(modTrans ? (〈[○,○];❨○,○❩〉) ?)
[ @modComm @(modTrans ? ([○,〈[○,○];❨○,○❩〉]) ?) [ @modComm @modParUnit |
@modParCom ]
| @modComm @(modTrans ? (〈[○,○];○〉) ?) [ 
@(modTrans ? ([○,○]) ?) [
@modComm @modParUnit |
@modComm @modSeqUnit2 ] |
@(modSeqContext2 (○) ([○,○]) (❨○,○❩) ) @modComm @modCoparUnit qed.



inductive rules : 𝐒 → 𝐒→ Prop ≝
| q : ∀R,S,T,U. rules ([〈R;S〉,〈T;U〉]) (〈[R,T];[S,U]〉).


(*

([〈R;S〉,〈T;U〉]) → (〈T;U〉,[〈R;S〉]) ⤳  (〈[T,R];[U,S]〉)


*)
(* (A,B)/〈A,B〉/[A,B]
    ○/[¬R,R]
    〈R,T〉 /[〈R,¬a〉, 〈a,T〉]
    
*)
(*
definition reach ≝ λS1,S2:𝐒. match S1 with 
[〈R;S〉,〈T;U〉] ⇒  True
| _ ⇒ False

].
*)

